COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(commentl EKL axioms for forms of Y combinator)
C00003 ENDMK
C⊗;
(commentl EKL axioms for forms of Y combinator)

(decl y1 |((ground→ground)→(ground→ground))→(ground→ground)| constant)

(decl tau |(ground→ground)→(ground→ground)|variable)

(decl f |ground→ground| variable)

(axiom |∀tau.lispcont(tau) ⊃ ∀u.tau(y1(tau))(u) = y1(tau)(u)|)

(define tauapp